finite{-}type($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$n$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow$$T$). Surj($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$; $T$; $f$)